Section: Scientific Foundations

Automated deduction

Participants : Sylvain Conchon, Évelyne Contejean, Claire Dross, Mohamed Iguernelala, Stéphane Lescuyer, Claude Marché, Alain Mebsout, Andrei Paskevich, Xavier Urbain.

Our group has a long tradition of research on automated reasoning, in particular on equational logic, rewriting, and constraint solving. The main topics that have been under study in recent years are termination proofs techniques, the issue of combination of decision procedures, and generation of proof traces. Our theoretical results are mainly materialized inside our two automated provers CiME and Alt-Ergo.

Termination

On the termination topic, we have studied new techniques which can be automated. A fundamental result of ours is a criterion for checking termination modularly and incrementally  [94] , and further generalizations  [84] . These criteria and methods have been implemented into the CiME2 rewrite toolbox  [63] . Around 2002, several projects of development of termination tools arose in the world. We believe we have been pioneer in this growth, and indeed we organized in 2004 the first competition of such tools.

A direction of research on termination techniques was also to apply our new approaches (for rewriting) to other computing formalisms, first to Prolog programs [89] and then to membership equational programs  [67] , a paradigm used in the Maude system  [45] .

Decision Procedures

Combination

Our research related to combination of decision procedures was initiated by a result [70] obtained in collaboration with Shankar's group at SRI-international who develops the PVS environment, showing how decision procedures for disjoint theories can be combined as soon as each of them provides a so-called “canonizer” and a “solver”. Existing combination methods in the literature are generally not very well understood, and S. Conchon had a major contribution, in collaboration with Sava Krstić from OGI School of Science and Engineering (Oregon Health and Science University, USA), which is a uniform description of combination of decision procedures, by means of a system of inference rules, clearly distinguished from their strategy of application, allowing much clearer proofs of soundness and completeness [9] , [60] .

Polymorphic Logics

In the specific domain of program verification, the goals to be proved are given as formulae in a polymorphic multi-sorted first-order logic. Some of the sorts, such as integers and arrays, are built-in as they come from the usual data-types of programming languages. Polymorphism is used as a convenience for defining the memory models of C and Java programs and is handled at the level of the Why tool.

In order to be able to use all the available automated theorem provers (Simplify, SMT provers), including those which handle only untyped formulae (Simplify), one has to provide a way to get rid of polymorphism.

S. Conchon and É. Contejean have proposed an encoding of polymorphic multi-sorted logic (PSL) into unsorted logic based on term transformation, rather than addition of sort predicates which was used till then. This approach was extended further by S. Lescuyer  [79] , J.-F. Couchot  [65] , N. Stouls  [64] .

The Alt-Ergo theorem prover

It would be more convenient to deal with polymorphism directly in the theorem prover. There was no such prover available at the beginning of 2006, that is why S. Conchon and É. Contejean decided to develop a new tool called Alt-Ergo which is dedicated to the resolution of polymorphic and multi-sorted proof obligations and takes as input the Why syntax. In 2011, Alt-Ergo is still the only existing prover dealing with parametric polymorphism.

Alt-Ergo is based on CC($X$) [3] , a generic congruence closure algorithm developed in the team, for deciding ground formulas in the combination of the theory of equality with uninterpreted symbols and an arbitrary built-in solvable theory $X$. Currently, CC($X$) can be instantiated by the empty equational theory, by the linear arithmetics and the theory of constructors.

Alt-Ergo contains also a Fourier-Motzkin decision procedure for linear arithmetics inequalities, a home-made SAT-solver and an instantiation mechanism.

The architecture of Alt-Ergo is modular: each part is described by a small set of inference rules and is implemented as an OCaml functor. Moreover, the code is short ($\sim$ 10000 lines).

Automated proofs and certificates

A common issue to both termination techniques and decision procedures is that automatic provers use complex algorithms for checking validity of formula or termination of a computation, but when they answer that the problem is solved, they do not give any more useful information. It is highly desirable that they give a proof trace, that is some kind of certificate that could be double-checked by a third party, such as an interactive proof assistant like Coq. Indeed Coq is based on a relatively small and stable kernel, so that when it checks that a proof is valid, it can be trusted. Morevoer, a subpart of Coq has been proven correct in Coq  [52] .

Coccinelle and CiME's traces

In addition to efficient termination techniques, CiME implements in particular a semi-decision procedure for the equality modulo a set of axioms, based on ordered completion. In 2005, the former human readable proof traces have been replaced by Coq certificates, based on reified proof objects for a FOL logic modelled inside Coq  [61] .

É. Contejean, A. Paskevich, X. Urbain and the Cédric participants of the A3PAT project, Pierre Courtieu, Olivier Pons (CNAM), and Julien Forest, (ENSIIE) develop the new version of the CiME tool, CiME 3, associated with a Coq library called Coccinelle developed by É. Contejean. A trace generator outputs a trace for Coq in the unified framework provided by the Coccinelle library [62] [4] . Coccinelle contains the corresponding modelling of terms algebras and rewriting statements, and also some generic theorems which are needed for establishing a rewriting property from a trace. For example, in order to produce a certificate of termination for a rewriting system, one may provide as a trace an ordering that contains the rewrite system, but it is also needed to have a proof that this ordering is well-founded. Such a proof (for RPO for instance) is part of Coccinelle as a generic property. Coccinelle also contains as generic theorems some powerful criteria of termination: dependency pairs [48] , the main modularity theorem for termination presented in the thesis of Urbain [94] as well as innermost termination, dependency pairs for it and its equivalence with standard termination in some specific cases [72] .

The main improvement over the previous approach  [61] is that the Coq development is parameterized with respect to the equality predicate (instead of using the Coq native equality). This allows to deal uniformly with equality modulo a set of axioms, with termination of a set of rewrite rules, and with rewriting modulo a set of equations, such as associativity-commutativity.

Certifying termination proofs gained interest in the term rewriting community. Groups are either developing their own certifier, or producing traces for other's, thanks to a shared XML format. Since 2007, the termination competition has a category for certified termination proofs.

Further note that our efforts are not limited to termination proofs, and to date CiME 3 is the only tool able to prove and to certify confluence of term rewriting systems [25] .

The ergo tactics

In his thesis [14] , S. Lescuyer proposed new automation capabilities for the Coq proof assistant. He obtains this mechanization via an integration into Coq of decision procedures for propositional logic, equality reasoning and linear arithmetic which make up the core of the Alt-Ergo SMT solver. This integration is achieved through the reflection technique, which consists in implementing and formally proving these algorithms in Coq in order to execute them directly in the proof assistant. Because the algorithms formalized in Coq are exactly those in use in Alt-Ergo's kernel, this work significantly increases our trust in the solver. In particular, it embeds an original algorithm for combining equality modulo theory reasoning, called CC(X) and inspired by the Shostak combination algorithm, and whose justification is quite complex.

The Coq implementation of S. Lescuyer is available in the form of tactics which allow one to automatically solve formulae combining propositional logic, equality and arithmetic. In order to make these tactics as efficient as may be, he has taken special care with performance in his implementation, in particular through the use of classical efficient data structures, which we provide as a separate library.